A, B:Realizer. A  B  R-Feasible(B)  R-Feasible(A)  [[A]]  [[B]] 

latex

Definitions

x:A. B(x), P  Q, t  T, AB, A, False, ij, SQType(T), {T}, Prop, [[R]], , , , A  B, Y, if b t else f fi, P & Q, P  Q, true, false, P  Q, R-Feasible(R), d-empty()

Lemmas

nat wf, R-size wf, nat plus wf, R-Feasible wf, R-sub wf, es realizer wf, le wf, nat properties, ge wf, bool cases, Rnone? wf, bool sq, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, Rnone-implies, d-sub-null, R-Dsys wf, Rplus? wf, R-size-decreases, Rplus-implies, Rplus-left wf, Rplus-right wf, R-compat-implies, dsys-join-sub, d-sub transitivity, m-sys-join wf2, dsys-sub-join-left, dsys-sub-join-right, d-sub-self, d-sub wf